Nuprl Lemma : mon_hom_p_id
13,42
postcript
pdf
g
:GrpSig. IsMonHom{
g
,
g
}(Id{|
g
|})
latex
Up
groups
1
Definitions of Statement
IsMonHom{
M1
,
M2
}(
f
)
Definitions
t
T
,
Id
,
x
f
y
,
FunThru2op(
A
;
B
;
opa
;
opb
;
f
)
,
P
&
Q
,
Id{
T
}
,
IsMonHom{
M1
,
M2
}(
f
)
,
x
:
A
.
B
(
x
)
Lemmas
grp
sig
wf
,
grp
id
wf
,
grp
car
wf
,
grp
op
wf
origin
g:GrpSig. IsMonHom{g,g}(Id{|g|}) g:GrpSig. IsMonHom{g,g}(Id{|g|}) 
Tx:A. B(x)